rcv{-}it(${\it ff}$; $p$; $e$; $i$; $j$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$((fifoR(${\it ff}$)($i$,$e$)) $\wedge$ (fifoS(${\it ff}$)($j$,$i$,fifoSender(${\it ff}$)($i$,$e$)))) $\wedge$ ($p$(fifoSender(${\it ff}$)($i$,$e$)))